A, B, C:MsgA. ma-frame-compat(C;A)  ma-frame-compat(C;B)  ma-frame-compat(C;A  B) 

latex

Definitions

x:A. B(x), P  Q, ma-frame-compat(A;B), M1  M2, P & Q, xdom(f). v=f(x)   P(x;v), t.1, t.2, M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), State(ds), mk-ma, M.state, M.da(a), (s1  s2 mod x), M.dout(l,tg), M.ds(x), t  T, Top, , x. t(x), if b then t else f fi , tt, ff, z != f(x)  P(a;z), MsgA, Valtype(da;k), P  Q, A, P  Q, x(s), , Unit, False,

Lemmas

ma-frame-compat wf, msga wf, fpf-join-dom, Id wf, Knd wf, id-deq wf, fpf-join-ap-sq, fpf-trivial-subtype-top, fpf-dom wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-join wf, top wf, fpf-cap wf, Kind-deq wf, locl wf, pi2 wf, pi1 wf, product-deq wf